r:, s:{s':| CoPrime(r,s') }, a, b:. x:. ((x = a mod r) & (x = b mod s)) 

latex

Definitions	Prop, CoPrime(a,b), x:A. B(x), t  T, , x:A. B(x), SqStable(P), P  Q, T, True, P & Q, a = b mod m, P  Q, P  Q
Lemmas	true wf, squash wf, eqmod weakening, multiply functionality wrt eqmod, add functionality wrt eqmod, eqmod functionality wrt eqmod, eqmod wf, gcd p sym, chrem exists aux a, sq stable coprime, nat plus wf, coprime wf